$\forall$${\it es}$:ES, $i$:Id. Choose($i$) $\in$ $b$:Id$\rightarrow$($x$:Id$\rightarrow$vartype($i$;$x$))$\rightarrow$(kindtype($i$;locl($b$))+Unit)